/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General License for more details.
 *
 * You should have received a copy of the GNU General License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.symm;

import java.util.Collections;
import java.util.Iterator;
import java.util.Map;
import java.util.Set;
import java.util.SortedSet;
import java.util.TreeMap;
import java.util.TreeSet;

import alloy.type.BasicType;
import alloy.util.Dbg;
import alloy.util.Util;

/**
 * Keep track of the available symmetry among basic type atoms,
 * as we do symmetry-breaking.  Initially, by Alloy semantics, each
 * basic type consists of a set of interchangeable atoms.  During
 * symmetry breaking this changes.  This class helps us keep track
 * of which {@link Symmetry}s are still true symmetries of the model.
 */
class AvailableSymmetry {
    /**
     * {@link Map} from {@link BasicType} to {@link Set} of {@link AtomSet}s of
     * {@link Integer} indices of interchangeable atoms.  The atoms within each
     * {@link AtomSet} are interchangeable.  Initially, Alloy semantics tells us
     * that for each {@link BasicType} we will have one {@link SortedSet} containing
     * all the indices (atoms).
     */
    private Map /* BasicType->Set[AtomSet] */ _btype2SymmSets = new TreeMap();

    //////////////
    // Methods //
    ////////////

    /**
     * Construct an {@link AvailableSymmetry} object for keeping track
     * of the remaining symmetry.  In the object after construction,
     * all atoms of each {@link BasicType} are interchangeable.
     */
    AvailableSymmetry(Set /* of BasicType */ basicTypes_) {
	for (Iterator basicTypeIter = basicTypes_.iterator(); basicTypeIter.hasNext();) {
	    BasicType btype = (BasicType)basicTypeIter.next();
	    Set /* of AtomSet */ btypeAtomSets = new TreeSet();
	    AtomSet allAtoms = new AtomSet(0, btype.getScope());
	    btypeAtomSets.add(allAtoms);
	    _btype2SymmSets.put(btype, btypeAtomSets);
	}
    }

    /**
     * Test whether the given {@link Symmetry} is available.
     */
    boolean isAvailable(Symmetry symm_) {
	// Test that each atom is mapped to a symmetric atom
	for (Iterator btIter = symm_.getPermutedTypes().iterator(); btIter.hasNext();) {
	    BasicType btype = (BasicType)btIter.next();
	    Set /* of AtomSet */ symmSets = (Set)_btype2SymmSets.get(btype);
	    for (int atom=0; atom<btype.getScope(); atom++) {
		int targetAtom = symm_.getTargetAtom(btype, atom);
		if (symmSets==null) {
		    if (targetAtom != atom) return false;
		} else {
		    // find the symmset containing atom,
		    // and check that targetAtom is also
		    // in the same symmset
		    boolean symmSetFound = false;
		    for (Iterator symmSetIter = symmSets.iterator(); !symmSetFound && symmSetIter.hasNext();) {
			AtomSet symmSet = (AtomSet)symmSetIter.next();
			if (symmSet.contains(atom)) {
			    if (!symmSet.contains(targetAtom)) return false;
			    symmSetFound = true;
			}
		    }
		    if (!symmSetFound
			// the atom is not part of a symmset --
			// then it is only symmetric to itself so
			// must map to itself
			&& targetAtom!=atom) return false;
		}  // there are some symmsets
	    }  // loop over atoms
	}  // loop over basic types
	return true;
    }  // isAvailable()
    
    /**
     * For the given {@link BasicType}, return a {@link Set} of {@link AtomSet}s
     * of interchangeable atoms.
     */
    Set /* of AtomSet */ getSymmSets(BasicType basicType_) {
	Set /* of AtomSet */ result = (Set)_btype2SymmSets.get(basicType_);
	return result==null ? Collections.EMPTY_SET : Collections.unmodifiableSet(result);
    }
    
    /**
     * Remove the given {@link AtomSet} of interchangeable atoms from the given
     * {@link BasicType}.  This means that the atoms are no longer interchangeable.
     * If some subsets of the given atom set are still interchangeable, you
     * can add them back individually by calling {@link #addAtomSet} on these
     * smaller subsets.
     */
    void removeSymmSet(BasicType basicType_, AtomSet atomSet_) {
	Set /* of AtomSet */ btAtomSets = (Set)_btype2SymmSets.get(basicType_);
	btAtomSets.remove(atomSet_);
    }

    /**
     * Remove all symmetry from a given {@link BasicType} -- this indicates
     * that all atoms of this basic type are distinguishable.
     */
    void removeAllSymmetry(BasicType basicType_) {
	Set /* of AtomSet */ btAtomSets = (Set)_btype2SymmSets.get(basicType_);
	btAtomSets.clear();
    }

    /** Test whether ALL atoms of the given {@link BasicType} are fully interchangeable. */
     boolean isFullySymmetric(BasicType basicType_) {
	Set /* of AtomSet */ btAtomSets = (Set)_btype2SymmSets.get(basicType_);
	if (btAtomSets.size() != 1) return false;
	AtomSet atomSet = (AtomSet)btAtomSets.iterator().next();
	return atomSet.size() == basicType_.getScope();
    }

    /**
     * Record the fact that the given atoms of a given {@link BasicType}
     * are fully interchangeable.
     */
    void addSymmSet(BasicType basicType_, AtomSet symmSet_) {
	if (symmSet_.size() > 1) {
	    Set /* of AtomSet */ btSymmSets = (Set)_btype2SymmSets.get(basicType_);
	    // check that the set does not intersect any other sets we already have --
	    // it shouldn't
	    for (Iterator symmSetIter = btSymmSets.iterator(); symmSetIter.hasNext();) {
		AtomSet oldSymmSet = (AtomSet)symmSetIter.next();
		Dbg.chk(!Util.setsIntersect(oldSymmSet.atoms(), symmSet_.atoms()));
	    }
	    btSymmSets.add(symmSet_);
	}
    }
}
